$\forall$${\it es}$:event\_system\{i:l\}, $x$,$y$:es{-}E(${\it es}$).
\\[0ex]($x$ rel\_plus(es{-}E(${\it es}$); ($\lambda$$x$,$y$. ($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$)))) $y$)
\\[0ex]$\Rightarrow$ (loc($x$) = loc($y$) $\in$ Id)